Added CBMC proof of stringBuilder function #255
Merged
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Co-authored-by: Aniruddha Kanhere <[email protected]>
* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace Co-authored-by: Aniruddha Kanhere <[email protected]>
* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setDataInterface function * removed unnecessary variables * Updated documentation * Uncrustified * Updated year in copyright notice Co-authored-by: Aniruddha Kanhere <[email protected]>
* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Add CBMC proof of OTA_HTTP_strerror function * Removed extra line and updated error log * Updated error log Co-authored-by: Aniruddha Kanhere <[email protected]>
* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC Proof of requestDataBlock_Http function * Removed extra line * Update Comments Co-authored-by: Aniruddha Kanhere <[email protected]>
* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for OTA_MQTT_strerror function * Removed extra line * Updated comments * Fixed formatting errors * Updated error log Co-authored-by: Aniruddha Kanhere <[email protected]>
* Add CBMC-proofs infrastructure * Added value to not update the submodule * Added Include paths and preprocessor defines * Added template define file * Updated to ignore the output files on git push * Added words * Updated Project Name * Updated source directory path * Add checks on the branch * Updated Submodule update value * Added litani submodule update * Update Project name Co-authored-by: Aniruddha Kanhere <[email protected]> * Added new line in the end of the file * Remove whitespace * Added CBMC proof for setControlInterface function * Removed extra line * Added macro for the function * Fix formating errors * Fix spell check errors * Added preprocessor definition for setControlInterface function Co-authored-by: Aniruddha Kanhere <[email protected]>
yanjos-dev
reviewed
Sep 1, 2021
Comment on lines
33
to
34
| /* The minimum and the maximum number of strings inside the numStrings is 11. */ | ||
| __CPROVER_assume( numStrings > 0 && numStrings < UINT32_MAX ); |
There was a problem hiding this comment.
This wording sounds like you are saying both the min and the max are 11. I think you mean to say that the min is 0 and the max is 11.
Also, if the max is 11, then why have the assumption go to UINT32_MAX? size_t is also a signed data type, so it doesn't make sense to compare it to UINT32_MAX.
yanjos-dev
suggested changes
Sep 1, 2021
Comment on lines
43
to
46
| for( i = 0; i < numStrings - 1; ++i ) | ||
| { | ||
| strings[ i ] = ( char * ) malloc( stringSize ); | ||
| } |
There was a problem hiding this comment.
This condition: i < numStrings - 1 is allocating only four strings, even if numStrings is 5. I think you want i < numStrings instead. This would match the previous malloc you did, where you allocated space for numStrings (in this ex. 5). This will also match the free statement that you have down below.
There was a problem hiding this comment.
Yes. I have changed the free statement accordingly. In this proof I only to allocate memory for the first numStrings-1 pointers.The previous malloc is allocate memory to store the pointers, In strings array the last pointer should always be a NULL pointer and that is why I have assumed the last pointer to be NULL.
| /* Free the allocated memory. */ | ||
| free( pBuffer ); | ||
|
|
||
| for( i = 0; i < numStrings; ++i ) |
There was a problem hiding this comment.
This should match your previous memory allocation. I think this is correct though and that the malloc code needs to change, as commented above.
There was a problem hiding this comment.
Updated it in 6d32385
yanjos-dev
approved these changes
Sep 7, 2021
aggarg
approved these changes
Sep 9, 2021
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Description of changes:
Added all the files for CBMC proof of stringBuilder function,
By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.